/*
 * Alloy Analyzer
 * Copyright (c) 2002 Massachusetts Institute of Technology
 *
 * The Alloy Analyzer is free software; you can redistribute it and/or modify
 * it under the terms of the GNU General Public License as published by
 * the Free Software Foundation; either version 2 of the License, or
 * (at your option) any later version.
 *
 * The Alloy Analyzer is distributed in the hope that it will be useful,
 * but WITHOUT ANY WARRANTY; without even the implied warranty of
 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
 * GNU General Public License for more details.
 *
 * You should have received a copy of the GNU General Public License
 * along with the Alloy Analyzer; if not, write to the Free Software
 * Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA  02111-1307  USA
 */

package alloy.transl;

import java.util.Iterator;
import java.util.Map;
import java.util.TreeMap;

import alloy.ast.LeafId;
import alloy.bool.BooleanFormula;
import alloy.bool.PartialAssignment;
import alloy.type.BasicType;
import alloy.util.Dbg;
import alloy.util.MultiDimArray;
import alloy.util.MultiDimIter;

/**
 * Allocate Boolean variables to relations, by allocating one Boolean
 * variable to each tuple of a relation.  The Boolean variable represents
 * whether the tuple is present in an instance.  Thus there is a 1-1
 * correspondence between assigning a relational value to a relation
 * and assigning Boolean values to all the Boolean variables allocated to
 * the relation.
 * <p>
 * If the Int special signature is used, this class also allocates Boolean
 * variables for the integers corresponding to each atom of the Int signature.
 */
public class DefaultRelationAllocator extends RelationAllocator {
    /** Information about the translatable AST */
    protected ASTInfo _astInfo;

    /** Object that gives out fresh Boolean variable numbers */
    protected BoolVarAllocator _boolVarAllocator;

    /**
     * Record of translations of relations.
     * {@link Map} from {@link LeafId} of relation to an {@link ExprTransl}.
     */
    private Map /* LeafId->ExprTransl */ _rel2transl = new TreeMap();

    /**
     * Integer width -- the number of bits in the integers represented by
     * the special signature Int.
     */
    private int _intWidth;

    /**
     * For each Int atom, the IntTransl representing the corresponding integer.
     */
    private IntTransl[] _intAtomTransls;

    //////////////
    // Methods //
    ////////////


    public DefaultRelationAllocator(ASTInfo astInfo_, BoolVarAllocator boolVarAllocator_,  int intWidth_) {
    _astInfo = astInfo_;
    _boolVarAllocator = boolVarAllocator_;
    if (intWidth_ < 0)
        intWidth_ = 3;
    _intWidth = intWidth_;

    if (astInfo_.getIntType() != null) {
			// allocate Boolean variables for the integers corresponding to Int atoms

			// find the special BasicType object for the Int
			BasicType intType = astInfo_.getIntType();
			if (intType != null) {
				//System.out.println("Int type present with scope " +
				// intType.getScope() + " and width " + intWidth_);
				_intAtomTransls = new IntTransl[intType.getScope()];
				for (int i = 0; i < intType.getScope(); i++) {
					BooleanFormula[] intBits = new BooleanFormula[intWidth_];
					for (int j = 0; j < intWidth_; j++) {
						int freshBoolVar = _boolVarAllocator.allocBoolVar();
						intBits[j] = BooleanFormula.makeLit(freshBoolVar);
					}
					_intAtomTransls[i] = new IntTransl(intBits, true /* signed */);
				} // loop over Int atoms
			} // basic type for Int found
		} // intWidth non-negative


    //_computeProductSigTransls();
    }  // DefalutRelationAllocator()

    /**
	 * Pre-compute translations of relations declared in product signatures. The
	 * semantics of product signatures requires that we set all these relations
	 * to constants; this is more than just an optimization, else it would be
	 * implemented as a {@link alloy.symm.SymmetryBreakingMethod}.
	 */
//     private void _computeProductSigTransls() {
//  Map /* LeafId->Map[LeafId->MultiplicityExpr] */ productSigIdsToRels =
//      _astInfo.getCommand().productSigIdsToRels;
//  for (Iterator prodSigIter = productSigIdsToRels.entrySet().iterator(); prodSigIter.hasNext();) {
//      Map.Entry prodSigEntry = (Map.Entry)prodSigIter.next();
//      LeafId prodSigId = (LeafId)prodSigEntry.getKey();

//      // say that the SigExpr for the product sig contains all possible atoms
//      Dbg.chk(!_rel2transl.containsKey(prodSigId));
//      RelationType prodSigType = _astInfo.getLeafType(prodSigId);
//      Dbg.chk(prodSigType.numBasicTypes() == 1);
//      int prodSigScope = prodSigType.getBasicTypeAt(0).getScope();
//      MultiDimArray prodSigExprFormulas = new MultiDimArray(new int[]{prodSigScope});
//      Arrays.fill(prodSigExprFormulas.getFlatData(), BooleanFormula.TRUE);
//      _rel2transl.put(prodSigId, new ExprTransl(prodSigType, prodSigExprFormulas));

//      // build an iterator that will iterate over possible combinations of values
//      // of the product signature's fields
//      Map /* LeafId->MultiplicityExpr */ prodFieldMults = (Map)prodSigEntry.getValue();
//      int nfields = prodFieldMults.size();
//      QVarIterationInfo[] qvarInfos = new QVarIterationInfo[nfields];
//      int[] fieldScopes = new int[nfields];
//      LeafId[] fieldIds = new LeafId[nfields];
//      MultiDimArray[] fieldTransls = new MultiDimArray[nfields];
//      RelationType newFieldTypes[] = new RelationType[nfields];
//      int fieldNum = 0;
//      for (Iterator prodFieldIter = prodFieldMults.entrySet().iterator(); prodFieldIter.hasNext();) {
//      Map.Entry prodFieldEntry = (Map.Entry)prodFieldIter.next();
//      LeafId prodFieldId = (LeafId)prodFieldEntry.getKey();
//      MultiplicityExpr prodFieldMult = (MultiplicityExpr)prodFieldEntry.getValue();
//      RelationType fieldType = _astInfo.getLeafType(prodFieldId);

//      fieldTransls[fieldNum] = new MultiDimArray(fieldType.getScopes());
//      _rel2transl.put(prodFieldId, new ExprTransl(fieldType, fieldTransls[fieldNum]));

//      RelationType newFieldType = new RelationType();
//      newFieldTypes[fieldNum] = newFieldType;
//      for (int i=1; i<fieldType.numBasicTypes(); i++)
//          newFieldType.addBasicType(fieldType.getBasicTypeAt(i));
//      qvarInfos[fieldNum] =
//          QVarValGenerator.constructQVarIterationInfo(newFieldType,
//                              prodFieldMult,
//                              false /* not declared in comprehension */,
//                              _astInfo.getLeafRep(prodFieldId).nodeString());
//      fieldScopes[fieldNum] = qvarInfos[fieldNum].getBoolSwitchValues().length;
//      fieldIds[fieldNum] = prodFieldId;
//      fieldNum++;
//      }

//      int prodAtomNum = 0;
//      for (MultiDimIter valIter = new MultiDimIter(fieldScopes); valIter.hasNext();) {
//      int[] valInds = (int[])valIter.next();
//      for (int i=0; i<valInds.length; i++) {
//          qvarInfos[i].getBoolSwitch().setVarValue(qvarInfos[i].getBoolSwitchValues()[valInds[i]]);
//          ExprTransl vtransl = qvarInfos[i].getQVarTransl();
//          RelationType relType = _astInfo.getLeafType(fieldIds[i]);
//          int[] tupleInds = new int[relType.numBasicTypes()];
//          tupleInds[0] = prodAtomNum;
//          for (MultiDimIter fieldTupleIter = new MultiDimIter(newFieldTypes[i].getScopes());
//           fieldTupleIter.hasNext();) {
//          int[] fieldTupleInds = (int[])fieldTupleIter.next();
//          System.arraycopy(fieldTupleInds, 0, tupleInds, 1, fieldTupleInds.length);
//          fieldTransls[i].put(tupleInds,
//                      BooleanFormula.makeConst(vtransl.getTupleFormula(fieldTupleInds).interpret()));
//          }

//          qvarInfos[i].getBoolSwitch().clearVarValue();
//      }
//      prodAtomNum++;
//      }
//      Dbg.chk(prodAtomNum == prodSigScope);
//  }  // loop over the product signatures
//     }  // _computeProductSigTransls()

    /**
     * Allocate Boolean variables to represent the value of a relation.
     * Right now we just allocate one Boolean variable for each tuple
     * the relation may have; the meaning of the variable is that it's
     * true iff the tuple is in the relation.  Later we will also try
     * other encodings esp. for functional relations where a logarithmic
     * number of Boolean variables might suffice.
     */
    protected ExprTransl allocRelation(LeafId relId_) {
    // Normal case -- just allocate a Boolean variable to each
    // possible tuple of the relation.
    Dbg.chk(!_rel2transl.containsKey(relId_));
    int[] dims = _astInfo.getLeafType(relId_).getScopes();
    MultiDimArray formulas = new MultiDimArray(dims);
    for (MultiDimIter indIter = new MultiDimIter(dims); indIter.hasNext();) {
        int[] inds = (int[])indIter.next();

        int freshBoolVar = _boolVarAllocator.allocBoolVar();
//          System.out.println("alloc: " + freshBoolVar + " to " +
//                     _astInfo.getLeafRep(relId_).nodeString());
        BooleanFormula unitClause = BooleanFormula.makeLit(freshBoolVar);
        formulas.put(inds, unitClause);
    }
    return new ExprTransl(_astInfo.getLeafType(relId_), formulas);
    }

    public ExprTransl getRelationTransl(LeafId relId_) {
    ExprTransl result = (ExprTransl)_rel2transl.get(relId_);
    if (result == null)
        _rel2transl.put(relId_, result = allocRelation(relId_));
    return result;
    }

    /**
     * Return an {@link IntTransl} of the integer represented
     * by the specified atom of the Int signature.
     */
    public IntTransl getIntAtomTransl(int atomIdx_) {
    return _intAtomTransls[atomIdx_];
    }

    /** Return the width (in bits) of integers allocated to the Int atoms */
    public int getIntWidth() { return _intWidth; }

    public BoolVarAllocator getBoolVarAllocator() { return _boolVarAllocator; }

    /**
     * Simplify all {@link alloy.bool.BooleanFormula}s in translations of relations,
     * using the given {@link PartialAssignment}.  We do this after {@link alloy.symm symmetry-breaking}
     * was used to choose constant values for some of the Boolean variables allocated to relations,
     * without changing the satisfiability of the formula.
     */
    public void simplify(PartialAssignment pa_) {
    for (Iterator valsIter = _rel2transl.values().iterator(); valsIter.hasNext();) {
        ExprTransl relTransl = (ExprTransl)valsIter.next();
        relTransl.simplify(pa_);
    }
    }
}
